T:Type, f:((T List)), t, t':.
(t < t')  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t'))) 

latex

Definitions	concat(ll), x:A. B(x), t  T, S  T, reduce(f;k;as), Y, {i..j}, i  j < k, P & Q, P  Q, A  B, A, False,
Lemmas	concat-cons, append nil sq, iseg map, upto wf, le wf, upto iseg